%%% BinCons.oz
%
% This module uses the binary model of the field to propagate and
% search for solutions.  Each square of the mine field corresponds to
% a binary value, with 1 meaning the presence of a mine, 0 its
% absence.
%
% {BinCons.constraints F NR#NC NM ?Cs}
%    binds Cs to a stream describing binary constraints corresponding
%    to the symbolic field F.  The elements of Cs have the form sum(Is
%    K), where Is is a list of indexes, and K is the sum of the binary
%    variables whose index is in Is.
%
% BinCons.propagator
%    posts all the propagators corresponding to the binary constraints
%    of the stream Cs.  When binary variables are determined, the
%    information is propagated to the symbolic field F.
%
% BinCons.solver
%    solves the minesweeper problem.  It returns a binary field
%    containing the values common to all solutions, and free variables
%    where values differ in the solutions.  It also returns a field
%    with probabilities (floats), together with the number of
%    representatives found by search, and the number of solutions to
%    the whole problem.
%
functor
import
   FD
   Field      at 'Field.ozf'
   Game       at 'Game.ozf'
   LazySearch at 'LazySearch.ozf'

export
   Constraints
   Propagator
   Solver

define
   % creates a stream describing binary constraints corresponding to
   % the symbolic field F
   proc {Constraints F NR#NC NM ?Cs}
      P = {NewPort Cs}
      BoxI = {Field.coord NR#NC}.boxI
   in
      {Send P sum({List.number 1 {Width F} 1} NM)}
      {Record.forAllInd F
       proc {$ I X}
	  thread
	     case X of safe(K) then
		{Send P sum([I] 0)}
		{Wait K} {Send P sum({BoxI I 1} K)}
	     [] mine(_) then
		{Send P sum([I] 1)}
	     end
	  end
       end}
   end

   % propagates the binary constraints
   class Propagator from Game.switchable
      meth init(F Cs)
	 B = {FD.tuple {Label F} {Width F} 0#1}
	 BF = fun {$ I} B.I end
      in
	 % create propagators from Cs
	 thread
	    for sum(Is K) in Cs do
	       {Wait @enabled} {FD.sum {Map Is BF} '=:' K}
	    end
	 end
	 % put results back in F
	 F = {Record.map B fun {$ X} thread {Field.symbolic X} end end}
      end
   end

   % solves the binary problem
   class Solver
      attr
	 constraints: nil   % stack with all the constraints

      meth init(Cs)
	 thread
	    for C in Cs do Cr in Cr = constraints := C|Cr end
	 end
      end

      meth search(common: Common <= _
		  mean:   Mean   <= _
		  found:  Found  <= _
		  total:  Total  <= _)
	 Cons = {Reverse @constraints}
	 Vars = for sum(Is _) in Cons.2  append:A do {A Is} end
	 proc {Script B}
	    BF = fun {$ I} B.I end
	 in
	    B = {FD.tuple field {Length Cons.1.1} 0#1}
	    for sum(Is K) in Cons do {FD.sum {Map Is BF} '=:' K} end
	    {FD.distribute naive {Map Vars BF}}
	 end
	 
	 FoundC = {NewCell 0}
	 TotalC = {NewCell 0}
	 SumC   = {NewCell {FD.tuple field {Length Cons.1.1} 0#0}}
      in
	 for B in {LazySearch.all Script} do
	    Known Unknown
	    {List.partition {Record.toList B} IsDet Known Unknown}

	    K1 = {FoldL Known Number.'+' 0}   % squares known to be 1
	    U  = {Length Unknown}             % unknown squares
	    U1 = Cons.1.2 - K1                % how many mines left

		      
	    Mined = {Binomial U-1 U1-1}   % mined and total number
	    Total = {Binomial U U1}       % of solutions per square
	 in
	    FoundC := @FoundC + 1
	    TotalC := @TotalC + Total
	    SumC   := {Record.zip
		       @SumC
		       {Record.map B
			fun {$ X} if {IsDet X} then X*Total else Mined end end}
		       Number.'+'}
	 end

	 Found  = @FoundC
	 Total  = @TotalC
	 Common = {Record.map @SumC
		   fun {$ X}
		      case X of 0 then 0 [] !Total then 1 else _ end
		   end}
	 Mean   = {Record.map @SumC
		   fun {$ X} {IntToFloat X} / {IntToFloat Total} end}
      end
   end

   % computes the binomial number C(N,K)
   fun {Binomial N K}
      if K<0 then 0
      elseif K==0 orelse K==N then 1
      else {Binomial N-1 K-1} * N div K
      end
   end
end
